Nuprl Lemma : frequency_wf
11,40
postcript
pdf
T
:Type,
eq
:(
T
T
),
f
:(
T
),
x
:
T
,
p
:
,
q
:
. frequency(
f
;
x
) ~ (
p
/
q
)
latex
Definitions
Type
,
t
T
,
,
x
:
A
B
(
x
)
,
,
,
#$n
,
a
<
b
,
P
Q
,
False
,
A
,
A
B
,
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
.
B
(
x
)
,
n
+
m
,
{
i
..
j
}
,
P
&
Q
,
i
j
<
k
,
#{i<
j
|
f
i
eq
x
}
,
|
a
/
b
-
p
/
q
| < 1/
m
,
,
A
c
B
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
frequency(
f
;
x
) ~ (
p
/
q
)
Lemmas
ratio-dist
wf
,
seq-count
wf
,
le
wf
,
int
seg
wf
,
nat
plus
wf
,
nat
wf
,
bool
wf
origin
T:Type, eq:(T
T
), f:(
T), x:T, p:, q:
. frequency(f;x) ~ (p/q) 
T:Type, eq:(TT), f:(T), x:T, p:, q:. frequency(f;x) ~ (p/q) TB(x)
Q
A
B
x:A. B(x)
} j < k
B
B(x)
x:A. B(x)